Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    f(f(a,b),x)  → f(b,f(a,f(c,f(b,f(a,x)))))
2:    f(x,f(y,z))  → f(f(x,y),z)
There are 7 dependency pairs:
3:    F(f(a,b),x)  → F(b,f(a,f(c,f(b,f(a,x)))))
4:    F(f(a,b),x)  → F(a,f(c,f(b,f(a,x))))
5:    F(f(a,b),x)  → F(c,f(b,f(a,x)))
6:    F(f(a,b),x)  → F(b,f(a,x))
7:    F(f(a,b),x)  → F(a,x)
8:    F(x,f(y,z))  → F(f(x,y),z)
9:    F(x,f(y,z))  → F(x,y)
The approximated dependency graph contains one SCC: {3-9}.
Tyrolean Termination Tool  (0.17 seconds)   ---  May 3, 2006